%explain this section
In this section, we express the importance of finding bad smells, and what kinds of problems they may bring to DBC/JML developers. 
%explain example
As example, consider a document editing system for Latex-based~\cite{latex-book} papers. The system allows authors to write papers in collaboration, using a web-based interface. The internal structure includes classes such as: \code{Document}, \code{Section} and \code{Author}, among others. A simplified UML class diagram is shown in Figure~\ref{fig:UMLexample}.

%class diagram
\begin{figure}[ht]
\begin{center}
\leavevmode
\scalebox{0.55}{
\includegraphics{images/UMLexample.png}}
\caption{Online document editing system}
\label{fig:UMLexample}
\end{center}
\end{figure}

%java code for Document class - focus on invariant that uses private att
Focusing our investigation on the \code{Document} class, version control is a system requirement. We can define these versions as a list of objects in the first document object. It can be implemented as a private field in Java.

\begin{lstlisting}[frame=single,framerule=0pt,numbers=none]
public class Document {
	private ArrayList versions = new ArrayList();
	
	void changeVersion() {
		if (this.versions != null)
			versions.add(new Document(..));
	}
}
\end{lstlisting}

%relax to spec_public, show code
In order to specify a contract for users of this class, developers may introduce invariants over \code{Document} objects. A plausible invariant is to avoid states in which a document appears more than once into the list of versions. Following the DBC approach, the invariant is visible to other objects, so it can be specified with a JML public invariant. As long as \code{versions} is a private field, JML offers a modifier that allows the field to appear in public invariants, \code{spec\_public}, as showed in the next fragment.

\begin{lstlisting}[frame=single,framerule=0pt,numbers=none]
public class Document {
	private /*@ spec_public @*/ ArrayList 
      versions = new ArrayList();

	//@ public invariant !versions.contains(this);	
..}
\end{lstlisting}

%explain problems with spec_public
The contract for \code{Document} is syntactically correct, providing the desired constraint. However, some careful analysis raises a number of issues with encapsulation:
\begin{itemize}
	\item as contracts are part of the public interface, clients will use them as basis for development; in this case, clients rely on implementation details for the class, as the \code{ArrayList} field is visible;
	\item the contract relies on a private field when using the \code{Document} class. This scenario may cause classes to be harder to change, without affecting other classes.
\end{itemize}

%second smell - resolve problema 1, usa model field
Alternative designs can be applied to avoid encapsulation issues, with the same practical issues. The JML language allows developers to hide the internal details of a class from a contract and its clients. \textit{Model fields} can be used for this purpose, representing a more abstract view of class data, as they can be freely viewed by clients. The implementation for the model field must be provided by concrete, possibly private fields; the \code{\textbf{represents}} clause allows us to express functional abstractions between model and concrete fields. Model field types can be defined as immutable objects provided by the JML models API~\cite{jml-models-api}, which provides classes that emulate mathematical objects (including sets, bags and sequences). These types are appropriate for abstract fields; in this example, we use the \code{JMLEqualsSet} class, which implements a set of values.

\begin{lstlisting}[frame=single,framerule=0pt,numbers=none]
public class Document {
	private ArrayList _versions = new ArrayList();

	//@ public model JMLEqualsSet versions;
	//@ public invariant !versions.has(this);	
..}
\end{lstlisting}

%represents
A concrete definition for this model field must be provided by the class developer. Here, a \code{JMLEqualsSet} object is built from the elements in the concrete \code{\_versions} list. The following \code{represents} clause illustrates this approach, with a \emph{model method}. Model methods provide an useful abstraction for procedures and functions that will only be used within JML contracts. In this case, the method copies every element from the concrete list to the mathematical set, so the model field can be evaluated.

\begin{lstlisting}[frame=single,framerule=0pt,numbers=none]
public class Document {..
  //@ private represents versions <- 
  //@                      abstractVersions();
  
  /*@ private model pure JMLEqualsSet 
    @   abstractVersions() {
	  @ 	  JMLEqualsSet ret = new JMLEqualsSet();
		@   	Iterator it = _versions.iterator();
		@   	while (it.hasNext()) {
   	@		  	ret.insert(it.next());
		@ 	  }
		@ 	  return ret;}
	  @*/ 
..}
\end{lstlisting}

%bad - complex represents
In this particular scenario, the method may be an overkill, with a very operational way of filling the mathematical set. It would be hard to write and maintain such code for numerous methods. This clause can be refactored to a better solution by using methods from the JML models API itself (the \code{getVersions} method).    

\begin{lstlisting}[frame=single,framerule=0pt,numbers=none]
public class Document{ ..
  //@ private represents versionsSet <- 
  //@   JMLEqualsSet.convertFrom(getVersions());
..}
\end{lstlisting}

%field obsession
Regarding method contracts, in class \code{Section}, the \code{beginEdition} method locks the section for editing by request of a given author. The preconditions state that the section is unlocked and the requesting author is included as an author for the given document (which cannot be null). As postcondition, the contract guarantees that the section is locked after the call.

\begin{lstlisting}[frame=single,framerule=0pt,numbers=none]
public class Section {..
	/*@ requires !locked;
	  @ requires document.authors.has(author);
	  @ requires document != null;
	  @ ensures locked;
    @*/
	public void beginEdition(Author author){..}  
..}
\end{lstlisting}

%bad smell
We can notice the repetitive use of fields in the specification, even though it provides the correct behavior. As creating a model field for each concrete field clutters the class, an alternative can be found for better encapsulating internal details. A good option is using public getter method (if they do not exist, they could be created).

\begin{lstlisting}[frame=single,framerule=0pt,numbers=none]
public class Section {..
	/*@ requires !isLocked();
	  @ requires isAuthorIncludedInDoc(author);
	  @ requires getDocument() != null;
	  @ ensures isLocked();
    @*/
	public void beginEdition(Author author){..} 
..}
\end{lstlisting}

%final explanation
From this example, we believe that several correct contract parts can be considerably improved for DBC contexts. These ``bad smells'' are catalogued in this work, so efforts towards effective DBC development can take advantage on tool support for detecting these smells and refactorings can then be more effectively employed.
